Definitions | #$n, t T, n - m, x:A. B(x), {x:A| B(x)} , , x:A B(x), P  Q, final-iterate(f; x), b, A c B, False, A, A B,  b, s = t, prop{i:l}, , void, isect(A; x.B(x)), top, subtype(S; T), left + right, suptype(S; T), can-apply(f; x), x:A B(x), P Q, P   Q, Unit, x:A. B(x), SWellFounded(R(x;y)), Type,  x,y. t(x;y), p-graph(A; f), ge(i; j), -n, n + m, f(a), do-apply(f; x), a < b |